Nuprl Lemma : test22
11,40
postcript
pdf
n
:
.
m
:
. (
m
=
n
)
latex
Definitions
True
,
T
,
t
.1
,
has-value(
a
)
,
x
:
A
.
B
(
x
)
,
,
False
,
A
,
A
B
,
i
j
,
,
{
T
}
,
SQType(
T
)
,
P
Q
,
t
T
,
x
:
A
.
B
(
x
)
,
P
Q
,
Dec(
P
)
Lemmas
le
wf
,
ge
wf
,
nat
properties
,
decidable
int
equal
,
nat
wf
origin
n:
. 
m:. (m = n) n:. m:. (m = n) 
Tx:A. B(x)
A
B
j 
Q
Tx:A. B(x)
Q